Require Import Program.

(* utils.v *)
Inductive Unit: Set := unit: Unit.
Definition eq_dec T := forall x y:T, {x=y}+{x<>y}.

(*  prop.v *)
Section PropLogic. 
Variable Predicate: Type.

Inductive LP: Type :=
  LPPred: Predicate -> LP
| LPAnd: LP -> LP -> LP
| LPNot: LP -> LP.

Variable State: Type.
Variable Sat: State -> Predicate -> Prop.

Fixpoint lpSat st f: Prop :=
  match f with
    LPPred p  => Sat st p
  | LPAnd f1 f2  => lpSat st f1 /\ lpSat st f2
  | LPNot f1  => not (lpSat st f1)
  end.
End PropLogic.

Implicit Arguments lpSat.

Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
  match f with
    LPPred _ p => p2lp p
  | LPAnd _ f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
  | LPNot _ f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
  end.
Implicit Arguments LPTransfo.

(* time.v *)


(*Defines an abstract time domain with some operators and their properties. No attempt to minimize the number of axioms. Can be instanciated by discrete or dense time
*)
Variable Time: Set.
Variable Zero: Time.
Variable tle: Time -> Time -> Prop.
Variable tlt: Time -> Time -> Prop.
Variable tadd: Time -> Time -> Time.
Variable tsub: Time -> Time -> Time.
Variable tmin: Time -> Time -> Time.
Notation "t1 @<= t2" := (tle t1 t2) (at level 70, no associativity).
Notation "t1 @< t2" := (tlt t1 t2) (at level 70, no associativity).
Notation "t1 @+ t2" := (tadd t1 t2) (at level 50, left associativity).
Notation "t1 @- t2" := (tsub t1 t2) (at level 50, left associativity).
Notation "t1 @<= t2 @<= t3" := ((tle t1 t2) /\ (tle t2 t3)) (at level 70, t2 at next level).
Notation "t1 @<= t2 @< t3" := ((tle t1 t2) /\ (tlt t2 t3)) (at level 70, t2 at next level).

Variable tzerop: forall n, (n = Zero) + {Zero @< n}.
Variable tlt_eq_gt_dec: forall x y, {x @< y} + {x=y} + {y @< x}.
Variable tle_plus_l: forall n m, n @<= n @+ m.
Variable tle_lt_eq_dec: forall n m, n @<= m -> {n @< m} + {n = m}.


Variable tzerop_zero: tzerop Zero = inleft (Zero @< Zero) (refl_equal Zero).
Variable tplus_n_O: forall n, n @+ Zero = n.
Variable tlt_le_weak: forall n m, n @< m -> n @<= m.
Variable tlt_irrefl: forall n, not(  n @< n).
Variable tplus_nlt: forall n m, not (n @+ m @< n).
Variable tle_n: forall n, n @<= n.
Variable tplus_lt_compat_l: forall n m p, n @< m -> p @+ n @< p @+ m.
Variable tlt_trans: forall n m p, n @< m -> m @< p -> n @< p.
Variable tle_lt_trans: forall n m p, n @<= m -> m @< p -> n @< p.
Variable tlt_le_trans: forall n m p, n @< m -> m @<= p -> n @< p.
Variable tle_refl: forall n, n @<= n.
Variable tplus_le_0: forall n m, n @+ m @<= n -> m = Zero.
Variable Time_eq_dec: eq_dec Time.






(* tts.v  *)

Section TTS.

Variable State: Type.
(*defines the semantic domain of timed systems*)

Record TTS: Type := mkTTS {
  Init: State -> Prop;
  Delay: State -> Time -> State -> Prop;
  Next: State -> State -> Prop;
  Predicate: Type;
  Satisfy: State -> Predicate -> Prop
}.

(*Synchronous product of a collection of TTS*)

Definition TTSIndexedProduct Ind (tts: Ind -> TTS): TTS := {|
  Init st := forall i, Init (tts i) st;
  Delay st d st' := forall i, Delay (tts i) st d st';
  Next st st' := forall i, Next (tts i) st st';
  Predicate := { i: Ind & Predicate (tts i) };
  Satisfy st p := Satisfy (tts (projT1 p)) st (projT2 p)
|}.

Check TTSIndexedProduct.
End TTS.

Section SIMU_F.

Variables StateA StateC: Type.

Record mapping: Type := mkMapping {
  mState: Type;
  mInit: StateC -> mState;
  mNext: mState -> StateC -> mState;
  mDelay: mState -> StateC -> Time -> mState;
  mabs: mState -> StateC -> StateA
}.

Variable m: mapping.

Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := 
  LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f.

Theorem satProd: forall State Ind Pred (Sat: forall i, State -> Pred i -> Prop) (st:State) i (f: LP (Pred i)),
  lpSat (Sat i) st f
  <->
  lpSat
    (fun (st : State) (p : {i : Ind & Pred i}) => Sat (projT1 p) st (projT2 p)) st
     (addIndex Ind _ i f).
Proof.
  induction f.
  split.
  intros.
  simpl.
  apply H.
  intros.
  apply H.   
  simpl.
  intros.
  split.
  intros.
  intuition.
  intros.
  intuition.
  simpl.
  split.
  intuition.
  intros.
  intuition.
(*  原来的证明
induction f;
  simpl;
  intros;
  split;
 intros;
 intuition.*)
Qed.

Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))):
  {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) :=
  fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)).

Implicit Arguments trProd.
Require Import Setoid.

Theorem satTrProd:
  forall State Ind Pred (tts: Ind -> TTS State) 
    (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))) (st:State) (p: {i:Ind & (Pred i)}),
  lpSat (Satisfy _ (tts (projS1 p))) st (tr (projS1 p) (projS2 p))
  <->
  lpSat (Satisfy _ (TTSIndexedProduct _ _ tts)) st (trProd _ tts tr p).
Proof.
  unfold trProd. unfold TTSIndexedProduct. simpl. intros.
  rewrite (satProd State Ind (fun i => Predicate State (tts i))
                      (fun i => Satisfy _ (tts i))).
split. intros. apply H. intros. apply H. 

(* 原来的证明
  unfold trProd, TTSIndexedProduct; simpl; intros.
  rewrite (satProd State Ind (fun i => Predicate State (tts i))
                      (fun i => Satisfy _ (tts i))); tauto. *)
Qed.

Theorem simuProd: 
  forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
    (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
    (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
     (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) -> 
       simu _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
                  (trProd Pred tta tra) (trProd Pred ttc trc).
Proof.
  intros.
  apply simuPrf with (fun ex st => forall i, inv _ _ (ttc i) (tra i) (trc i) (X i) ex st); simpl; intros; auto.
  eapply invInit; eauto.
  eapply invDelay; eauto.
  eapply invNext; eauto.
  eapply simuInit; eauto.
  eapply simuDelay; eauto.
  eapply simuNext; eauto.
  split; simpl; intros.
  generalize (proj1 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
  rewrite <- (satTrProd StateA Ind Pred tta tra); apply H1.
  rewrite (satTrProd StateC Ind Pred ttc trc); apply H0.
  generalize (proj2 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
  rewrite <- (satTrProd StateC Ind Pred ttc trc); apply H1.
  rewrite (satTrProd StateA Ind Pred tta tra); apply H0.
Qed.
Check simuProd.
End SIMU_F.

Record simu_equiv StateA StateC m1 m2 Pred (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuEquivPrf {
  simuLR: simu StateA StateC m1 Pred a c tra trc;
  simuRL: simu StateC StateA m2 Pred c a trc tra
}.


Check simu_equivProd.

(*  aadl.v   *)

(*Here, we only consider periodic threads. A thread has a set of input data ports and a set of output data ports. At each activation, the thread computes the value of its outputs given the value of its input ports.
*)
Record Thread {Value:Type}: Type := mkThread {
  Period: Time;
  Period_gt0: Zero @< Period;
  IPort: Set;
  OPort: Set;
  Computation: (IPort -> Value) -> OPort -> Value;
  ComputationWF: forall v1 v2 o, (forall i, v1 i = v2 i) -> Computation v1 o = Computation v2 o
}.
(*
An AADL system is here seen as a set of connected threads. Each input port is connected to the output port of another thread.
*)
Record AADLSystem: Type := mkSystem {
  aValue: Type;
  thInd: Type;
  ind_eq_dec: eq_dec thInd;
  thread: thInd -> Thread (Value:=aValue);
  src: forall th, IPort (thread th) -> thInd;
  srcp: forall th i, OPort (thread (src th i))
}.

Section AADL_SEM.

Inductive ThState: Set := Idle | Dispatched.

Theorem ThState_eq_dec: eq_dec ThState.
Proof.
  unfold eq_dec.
  decide equality.
Defined.

Variable sys: AADLSystem.
(*
The state of an AADL system contains the contents of each port, the next dispatch time of each thread, the current time and the state of each thread
*)
Record AADLState: Type := mkAADLState {
  IVal: forall th, IPort (thread sys th) -> aValue sys;
  OVal: forall th, OPort (thread sys th) -> aValue sys;
  NextPeriod: thInd sys -> Time;
  Date: Time;
  TState: thInd sys -> ThState
}.
(*
Observers over an AADL model. An observer is defined by a predicate over the value of a port*)
Record ThreadPred (i:thInd sys): Type := mkThreadPred {
  thport: IPort (thread sys i) + OPort (thread sys i);
  thcond: aValue sys -> Prop
}.
(*
Evaluation of an observer over an AADL state*)
Definition ThreadSat th st (p: ThreadPred th): Prop :=
  match thport th p with
    inl ip => thcond th p (IVal st th ip)
  | inr op => thcond th p (OVal st th op)
  end.
(*
The set of observers over an AADL model is the union of observers of each thread*)
Definition AADLPred := { th : thInd sys & ThreadPred th}.
(*
Evaluation of AADL observers on an AADL state*)
Definition AADLSat st (p: AADLPred): Prop :=
  ThreadSat (projS1 p) st (projS2 p).
(*
Initial state of the AADL model*)
Record thInit (th: thInd sys) (st: AADLState): Prop := thInitPrf {
  thiDate: Date st = Zero;
  thiNextP: NextPeriod st th = Zero;
  thiState: TState st th = Idle
}.
(*
Thread behavior, untimed transitions
dispatch when state = idle: inputs copied from outputs
completion at end of period: update of output ports
computation between dispatch and completion*)

(*
thread behavior - timed transition time advance when thread is in the dispatched state. Ports are unchanged
*)
Inductive thDelay thd (st1: AADLState) d (st2: AADLState): Prop :=
| thWait: 
    TState st1 thd = Dispatched ->
    Date st1 @+ d @<= NextPeriod st1 thd ->
    Date st2 = Date st1 @+ d ->
    NextPeriod st2 thd = NextPeriod st1 thd ->
    (forall ip, IVal st2 thd ip = IVal st1 thd ip) ->
    (forall op, OVal st2 thd op = OVal st1 thd op) ->
    TState st2 thd = Dispatched ->
    thDelay thd st1 d st2.
(*
TTS of thread*)
Definition Thread_TTS th: TTS AADLState := mkTTS AADLState
  (fun st => thInit th st)
  (fun st1 d st2 => Zero @< d /\ thDelay th st1 d st2)
  (fun st1 st2 => thNext th st1 st2)
  (ThreadPred th)
  (ThreadSat th).
(*
TTS of an AADL system as a product of thread TTS*)
Definition AADL_TTS2: TTS AADLState :=
  TTSIndexedProduct AADLState (thInd sys) Thread_TTS.

End AADL_SEM.


(*ada*)
Definition Env Vars (Value:Vars->Type) := forall (v:Vars),Value v. 
Print Env.

Record Function {Vars:Type} {Value:Vars->Type} (Used:Vars->Type) := mkFunction {
  FDuration: Time;
  FCondition: Env Vars Value -> Prop;
  FComputation: Env Vars Value -> forall v:Vars,Used v -> Value v
}.

Record Task {Vars:Type} {Value:Vars->Type} :Type :=mkTask {
  Period_ada:Time;
  Period_gt0_ada:Zero @< Period_ada;
  Used:Vars -> Prop;
  FunId:Set;
  Funs:FunId -> Function (Value:=Value) Used;
  input:forall v, Used v -> Value v -> Prop
}.

Record AdaSystem: Type := mkAdaSystem {
  Vars:Type;
  Value:Vars->Type;
  TaskId: Type;
  task: TaskId -> Task (Value:=Value)
}.

Section Ada_SEM.
Variable sys:AdaSystem.

Inductive TaskState: Set := Ready | Running.
Theorem TaskState_eq_dec: eq_dec TaskState.
Proof.
  unfold eq_dec.
  decide equality.
Defined.

Record TaskUpdate: Type :=mkTU {
  date: Time;
  need: Vars sys -> Prop;
  update: forall v, need v ->Value sys v
}.

Record AdaState: Type := mkAdaState {
  currentTime: Time; 
  currentEnv: Env (Vars sys) (Value sys); 
  taskState: TaskId sys -> TaskState;
  taskupdate: TaskId sys -> TaskUpdate
}.


Record TaskPred (t : Task (Value := Value sys)):Type:=mkTaskPred {
  taskvars : Vars sys;
  taskUsed : Used t taskvars;
  test : Value sys taskvars -> Prop
}.

Definition TaskSat t st (p : TaskPred t):Prop:=
  match taskvars t p with
  | vars => test t p (currentEnv st (taskvars t p))
  end.

Definition AdaPred := { i : TaskId sys & TaskPred (task sys i)}.

Definition AdaSat st (p: AdaPred):Prop := TaskSat (task sys (projS1 p)) st (projS2 p).

Record taskInitWithUpdate (i: TaskId sys) (st: AdaState) : Prop := taskInitWithUpdatePrf {
  tInitTime: currentTime st = Zero;
  tInitState: taskState st i = Ready;
  tInitupdate: exists f, FCondition (Used (task sys i)) (Funs (task sys i) f) (currentEnv st)  /\ 
  taskupdate st i = (
  mkTU Zero (Used (task sys i)) (FComputation (Used (task sys i)) (Funs (task sys i) f) (currentEnv st)));
  tInitenv: forall v (u: Used (task sys i) v), input (task sys i) v u (currentEnv st v)
}.


Inductive taskNextWithUpdate (i: TaskId sys) st1 st2: Prop :=
  | taskDispatch: taskState st1 i = Ready -> currentTime st2 = currentTime st1
      -> (forall (tu:TaskUpdate), taskupdate st1 i = tu -> date tu = currentTime st2 -> forall (v:Vars sys) (u:need tu v),currentEnv st2 v = update tu v u)
      -> ( ~(forall tu, taskupdate st1 i = tu -> date tu = currentTime st1) -> taskupdate st2 i =taskupdate st1 i ) 
      -> (exists f, FCondition (Used (task sys i)) (Funs (task sys i) f) (currentEnv st2)  /\ 
         taskupdate st2 i = (mkTU (currentTime st2 @+ FDuration (Used (task sys i)) (Funs (task sys i) f)) (Used (task sys i)) (FComputation (Used (task sys i)) (Funs (task sys i) f) (currentEnv st2))))
      -> taskState st2 i = Running -> taskNextWithUpdate i st1 st2
  | taskComplete: taskState st1 i =Running -> currentTime st1 = date (taskupdate st1 i) -> currentTime st2 = currentTime st1
      -> (forall  (tu:TaskUpdate), taskupdate st1 i = tu -> date tu = currentTime st2 -> forall (v:Vars sys) (u:need tu v),currentEnv st2 v = update tu v u)
      -> ( ~(forall tu, taskupdate st1 i = tu -> date tu = currentTime st1) -> taskupdate st2 i =taskupdate st1 i ) 
      -> (exists f, FCondition (Used (task sys i)) (Funs (task sys i) f) (currentEnv st2)  /\ 
         taskupdate st2 i = (mkTU (currentTime st2 @+ FDuration (Used (task sys i)) (Funs (task sys i) f)) (Used (task sys i)) (FComputation (Used (task sys i)) (Funs (task sys i) f) (currentEnv st2))))
      -> taskState st2 i = Ready 
      -> taskNextWithUpdate i st1 st2
  | taskcompute: taskState st1 i = Running -> currentTime st1 @< date (taskupdate st1 i) -> currentTime st2 = currentTime st1
      -> (forall (v:Vars sys), Used (task sys i) v -> currentEnv st2 v = currentEnv st1 v)
      -> ((forall tu, taskupdate st1 i = tu -> currentTime st1 @<= date tu) -> taskupdate st2 i = taskupdate st1 i )
      -> taskState st2 i = Running -> date (taskupdate st2 i) = date (taskupdate st1 i) ->taskNextWithUpdate i st1 st2 
.



Inductive taskDelayWithUpdate (i: TaskId sys) (st1:AdaState) d (st2:AdaState):Prop :=
  | taskWait_run: taskState st1 i = Running -> currentTime st1 @+ d @<= date (taskupdate st1 i)
      -> currentTime st2 = currentTime st1 @+ d -> date (taskupdate st2 i) = date (taskupdate st1 i)
      -> taskupdate st2 i = taskupdate st1 i
      -> (forall (vars:Vars sys) ,Used (task sys i) vars -> currentEnv st2 vars = currentEnv st1 vars)
      -> taskState st2 i = Running -> taskDelayWithUpdate i st1 d st2
 (* | taskWait_ready: taskState st1 i = Ready -> currentTime st1 @+ d @<= NextDate st1 i
      -> currentTime st2 = currentTime st1 @+ d -> NextDate st1 i = NextDate st2 i
      -> (forall (vars:Vars sys) ,Used (task sys i) vars -> currentEnv st2 vars = currentEnv st1 vars)
      -> taskState st1 i = Ready -> taskDelay i st1 d st2 *)
.

Definition Task_TTS (i: TaskId sys): TTS AdaState := mkTTS AdaState
  (fun st => taskInitWithUpdate i st) 
  (fun st1 d st2 => Zero @< d /\ taskDelayWithUpdate i st1 d st2)
  (fun st1 st2 => taskNextWithUpdate i st1 st2)
  (TaskPred (task sys i)) (TaskSat (task sys i)).

Definition Ada_TTS2 (v:Vars sys): TTS AdaState := 
  TTSIndexedProduct AdaState (TaskId sys) Task_TTS.

End Ada_SEM.





Section AADL2Ada.

Variable sys:AADLSystem.

Inductive AdaVars: Type := 
  inputs: forall i, IPort (thread sys i) -> AdaVars
| outputs: forall i, OPort (thread sys i) -> AdaVars
| tstates: thInd sys -> AdaVars.

Definition AdaValue (v:AdaVars): Type :=
  match v with
    inputs i ip => aValue sys
  | outputs i op => aValue sys
  | tstates i => ThState
  end.

Inductive Rules: Set := rDispatch | rComplete.

Definition isUsed i v : Prop :=
  match v with
    inputs i1 ip => i = i1
  | outputs i1 op => i = i1
  | tstates i1 => i = i1
  end.

Definition doDispatch (i: thInd sys): Function (isUsed i):=
  mkFunction AdaVars AdaValue (isUsed i) Zero 
  (fun env => env (tstates i) = Idle )
  (fun env v h => match v return AdaValue v with
     tstates i1 => if ind_eq_dec sys i i1 then Dispatched else env (tstates i1)
   | outputs i1 op => env (outputs i1 op)
   | inputs i1 ip => if ind_eq_dec sys i i1 then env (outputs (src sys i1 ip) (srcp sys i1 ip))
                                            else env (inputs i1 ip)
end).

Definition doComplete (i: thInd sys): Function (isUsed i):=
  mkFunction AdaVars AdaValue (isUsed i) (Period (thread sys i)) 
  (fun env => env (tstates i) = Dispatched )
  (fun env v h => match v return AdaValue v with
     tstates i1 => if ind_eq_dec sys i i1 then Idle else env (tstates i1)
   | inputs i1 ip => env (inputs i1 ip)
   | outputs i1 op => if ind_eq_dec sys i i1 then (Computation (thread sys i1) (fun ip => env (inputs i1 ip)) op)
                                            else env (outputs i1 op)
end).

Definition Thread2Task (i: thInd sys): Task :=
  mkTask AdaVars AdaValue (Period (thread sys i)) (Period_gt0 (thread sys i)) (isUsed i) Rules 
  (fun r => match r with 
    rDispatch => doDispatch i
  | rComplete => doComplete i
  end)
  (fun v h => match v return AdaValue v -> Prop with
       inputs _ _ => fun _ => True
     | outputs _ _ => fun _ => True
     | tstates _ => fun w => w = Idle
  end).

Definition AADL2Ada: AdaSystem := 
  mkAdaSystem AdaVars AdaValue (thInd sys) Thread2Task.

Definition Sys2AdaEnv (st:AADLState sys): Env AdaVars AdaValue :=
  fun v => match v return AdaValue v with
      inputs  i ip => (IVal sys st i ip)
    | outputs i op => (OVal sys st i op)
    | tstates i => (TState sys st i)
  end.

Record getInvariant_AADL (i: thInd sys) (ext:Unit) (st: AADLState sys): Prop := mkInv {
  INP: TState sys st i = Idle -> NextPeriod sys st i = Date sys st
}.

Definition getTaskStates (st: AADLState sys) (i: thInd sys): TaskState :=
  match TState sys st i with
   Idle => Ready
 | Dispatched => Running
 end.

Definition getTaskUpdate (st: AADLState sys) (i: thInd sys): TaskUpdate AADL2Ada :=
  match TState sys st i with
    Idle =>
      (mkTU AADL2Ada (Date sys st)
        (isUsed i)
        (fun v c => 
        match v return AdaValue v with
          inputs i1 ip => (OVal sys st (src sys i1 ip) (srcp sys i1 ip))
        | outputs i1 op => (OVal _ st i1 op)
        | tstates i1 => Dispatched
      end
    ))
  | Dispatched => 
      (mkTU AADL2Ada (NextPeriod sys st i)
    (isUsed i)
    (fun v c => 
      match v return AdaValue v with
          inputs i1 ip => (IVal _ st i1 ip)
        | outputs i1 op => (Computation (thread sys i1) (IVal _ st i1) op)
        | tstates i1 => Idle
      end
    ))
  end.

Axiom env_eq: forall T1 T2 T3 (f g: forall (x:T1), T2 x -> T3 x), (forall x y, f x y = g x y) -> f = g.

Definition AADL2Ada_mapping: mapping (AdaState AADL2Ada) (AADLState sys) := mkMapping
  (AdaState AADL2Ada) (AADLState sys) Unit 
  (fun (st:AADLState sys) => unit)
  (fun (un: Unit) (st: AADLState sys) => unit)
  (fun (un: Unit) (st: AADLState sys) (d:Time) => unit)
  (fun (un: Unit) (st: AADLState sys) => mkAdaState AADL2Ada (Date sys st) (Sys2AdaEnv st) (getTaskStates st) (getTaskUpdate st)).

Definition AADLP2AdaP (i: thInd sys) (p:ThreadPred sys i): Predicate (AdaState AADL2Ada) (Task_TTS AADL2Ada i) :=
  match (thport sys i p) return TaskPred AADL2Ada (task AADL2Ada i) with
    inl ip => mkTaskPred AADL2Ada (task AADL2Ada i) (inputs i ip) eq_refl (thcond sys i p)
  | inr op => mkTaskPred AADL2Ada (task AADL2Ada i) (outputs i op)eq_refl (thcond sys i p)
  end.

Definition AADLP2AdaLP i (p:ThreadPred sys i): LP (Predicate (AdaState AADL2Ada) (Task_TTS AADL2Ada i)) :=
  LPPred _ (AADLP2AdaP i p).

Definition P2LP i p :=LPPred (Predicate (AADLState sys) (Thread_TTS sys i)) p.

Theorem Thread2Task_simu1_InvInit:forall (i : thInd sys)(st : AADLState sys),
Init (AADLState sys) (Thread_TTS sys i) st ->
getInvariant_AADL i
  (mInit (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping st) st.
Proof.
  simpl.
  intros.
  split.
  intros.
  inversion_clear H.
  rewrite thiDate0.
  trivial.
Qed.

Theorem Thread2Task_simu1_InvDelay:forall (i : thInd sys)(ex1 : mState (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping)
  (st1 st2 : AADLState sys) (d : Time),
Delay (AADLState sys) (Thread_TTS sys i) st1 d st2 ->
getInvariant_AADL i ex1 st1 ->
getInvariant_AADL i
  (mDelay (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping ex1 st1 d) st2.
Proof.
  simpl.
  intros.
  split.
  intros.
  inversion_clear H.
  inversion_clear H3.
  rewrite H9 in H1.
  discriminate H1.
Qed.

Theorem Thread2Task_simu1_InvNext:forall (i : thInd sys)(ex1 : mState (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping)
  (st1 st2 : AADLState sys),
Next (AADLState sys) (Thread_TTS sys i) st1 st2 ->
getInvariant_AADL i ex1 st1 ->
getInvariant_AADL i
  (mNext (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping ex1 st1) st2.
Proof.
  simpl.
  intros.
  split.
  intros.
  inversion_clear H. (*将会因为thNext而变为三个证明目标。*)
  (*第一个小目标*)
  rewrite H7 in H1.
  discriminate H1.
  (*第二个小目标*)
  rewrite <- H3 in H8.
  rewrite <- H4 in H8.
  trivial.
  (*第三个小目标*)
  rewrite -> H1 in H5.
  discriminate H5.
Qed.

Theorem Thread2Task_simu1_simuInit:forall (i : thInd sys)(st : AADLState sys),
Init (AADLState sys) (Thread_TTS sys i) st ->
Init (AdaState AADL2Ada) (Task_TTS AADL2Ada i)
  (mabs (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping
     (mInit (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping st) st).
Proof.
  simpl.
  intros.
  inversion_clear H.
  split. (*将依据taskInit分为三个情况*)
  (*第一个小目标*)
  simpl.
  trivial.
  (*第二个小目标*)
  simpl.
  unfold getTaskStates.
  rewrite thiState0.
  trivial.
  (*第三个小目标*)
  simpl.
  intros.
  exists rDispatch.
  simpl.
  split.
  trivial.
  unfold getTaskUpdate.
  rewrite thiState0.
  rewrite thiDate0.
  f_equal.
  apply env_eq.
  intro.
  case x.
  simpl.
  intros.
  case_eq (ind_eq_dec sys i i0).
  trivial.
  intros.
  contradiction n.
  simpl.
  trivial.
  simpl.
  intros.
  case_eq (ind_eq_dec sys i t).
  intros.
  trivial.
  intros.
  contradiction n.
  simpl.
  intro.
  case v.
  simpl.
  trivial.
  trivial.
  simpl.
  intros.
  rewrite <- u.
  trivial.
Qed.

Theorem Thread2Task_simu1_simuDelay:forall (i : thInd sys)(ex1 : mState (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping)
  (st1 st2 : AADLState sys) (d : Time),
Delay (AADLState sys) (Thread_TTS sys i) st1 d st2 ->
getInvariant_AADL i ex1 st1 ->
Delay (AdaState AADL2Ada) (Task_TTS AADL2Ada i)
  (mabs (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping ex1 st1) d
  (mabs (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping
     (mDelay (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping ex1 st1 d)  st2).
Proof.
  simpl.
  intros.
  inversion_clear H.
  inversion_clear H2.
  split.
  trivial.
  inversion_clear H0.
  apply taskWait_run. (*分成6个小目标*)
  (*第一个小目标*)
  simpl.
  unfold getTaskStates.
  rewrite -> H.
  trivial.
  (*第二个小目标*)
  simpl.
  unfold getTaskUpdate.
  simpl.
  rewrite H.
  simpl.
  apply H3.
  (*第三个小目标*)
  simpl.
  apply H4.
  (*第四个小目标*)
  simpl.
  unfold getTaskUpdate.
  simpl.
  rewrite H.
  rewrite H8.
  simpl.
  apply H5.
  (*第五个小目标*)
  simpl.
  unfold getTaskUpdate.
  simpl.
  rewrite H.
  rewrite H8.
  rewrite H5.
  f_equal.
  apply env_eq.
  intro.
  case x.
  simpl.
  intros.
  revert i1.
  rewrite <- y.
  apply H6.
  simpl.
  intros.
  revert o.
  rewrite <- y.
  intros.
  apply ComputationWF.
  trivial.
  trivial.
  simpl.
  unfold Sys2AdaEnv.
  simpl.
  intro.
  case vars.
  simpl.
  intros.
  revert i1.
  rewrite <- H0.
  trivial.
  simpl.
  intros.
  revert o.
  rewrite <- H0.
  trivial.
  simpl.
  intros.
  rewrite <- H0.
  rewrite H,H8.
  trivial.
  simpl.
  unfold getTaskStates.
  rewrite H8.
  trivial.
Qed.

Theorem Thread2Task_simu1_simuNext:forall (i : thInd sys)(ex1 : mState (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping)
  (st1 st2 : AADLState sys),
Next (AADLState sys) (Thread_TTS sys i) st1 st2 ->
getInvariant_AADL i ex1 st1 ->
Next (AdaState AADL2Ada) (Task_TTS AADL2Ada i)
  (mabs (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping ex1 st1)
  (mabs (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping
     (mNext (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping ex1 st1) st2).
Proof.

  simpl.
  intros.
  inversion_clear H0.
  inversion_clear H. (*依据thNext分解成为3个小目标*)
  (*第一个小目标*)
  apply taskDispatch.
  simpl.
  unfold getTaskStates.
  rewrite -> H0.
  trivial.
  simpl.
  trivial.
  
  simpl.
  intros.
  unfold getTaskUpdate in H.
  rewrite H0 in H.
  unfold Sys2AdaEnv.
  revert u.
  rewrite <- H.
  simpl. case v.
  simpl. intros. revert i1. rewrite <- u. trivial.
  simpl. intros. revert o. rewrite <- u. trivial.
  simpl. intros. rewrite <- u. trivial.
  
  simpl. intros. contradiction H. clear H.
  unfold getTaskUpdate. rewrite H0.
  simpl. intros. rewrite <- H.
  simpl. trivial.
  
  exists rComplete.
  simpl. rewrite H5. 
  split.
  trivial.
  unfold getTaskUpdate.
  rewrite H5.
  simpl.
  rewrite H4,(INP0 H0),H1.
  f_equal.
  apply env_eq.
  intro.
  case x.
  simpl. trivial.
  simpl. intros. 
  case_eq(ind_eq_dec sys i i0).
  simpl. intros. apply ComputationWF. trivial.
  intros. contradiction n.
  simpl. intros.
  case_eq (ind_eq_dec sys i t).
  intros. trivial.
  intros. contradiction n.
  
  simpl. unfold getTaskStates. rewrite H5. trivial.

  (*第二个小目标*)
  apply taskComplete.
  simpl.
  unfold getTaskStates.
  rewrite H0.
  trivial.
  simpl.
  unfold getTaskUpdate.
  rewrite H0.
  simpl.
  trivial.
  simpl.
  trivial.
  simpl.
  unfold getTaskUpdate.
  rewrite H0.
  unfold Sys2AdaEnv.
  intros.
  revert u H7.
  rewrite <- H.
  simpl.
  case v.
  simpl. intros. revert i1. rewrite <- u. trivial.
  simpl. intros. revert o. rewrite <- u. trivial.
  simpl. intros. rewrite <- u. trivial.

  simpl. intros. contradiction H. clear H.
  unfold getTaskUpdate. rewrite H0.
  simpl. intros. rewrite <- H.
  simpl. symmetry. trivial.
  
  exists rDispatch.
  simpl. rewrite H3. 
  split.
  trivial.
  unfold getTaskUpdate.
  rewrite H3.
  simpl.
  rewrite (tplus_n_O (Date sys st2)).
  f_equal.
  apply env_eq.
  intro.
  case x.
  simpl. trivial.
  simpl. intros. 
  case_eq(ind_eq_dec sys i i0).
  simpl. intros. trivial.
  intros. contradiction n.
  simpl. intros. trivial.
  simpl. intros.
  case_eq (ind_eq_dec sys i t).
  intros. trivial.
  intros. contradiction n.
  
  simpl. unfold getTaskStates. rewrite H3. trivial.
  (*第三个目标*)
  apply taskcompute.
  simpl. unfold getTaskStates. rewrite H0. trivial.
  simpl. unfold getTaskUpdate. rewrite H0. simpl. trivial.
  simpl. trivial.
  simpl. intro. 
  case v.
  simpl. intros. revert i1. rewrite <- H. trivial.
  simpl. intros. revert o. rewrite <- H. trivial.
  simpl. intros. rewrite <- H. rewrite H0,H3. trivial.
  simpl. unfold getTaskUpdate. rewrite H0,H3.
  intros. f_equal. trivial.
  apply env_eq.
  intro. case x.
  simpl. intros. revert i1. rewrite <- y. trivial.
  simpl. intros. revert o. rewrite <- y. intros. apply ComputationWF. trivial.
  simpl. trivial.
  simpl. unfold getTaskStates. rewrite H3. trivial.
  simpl. unfold getTaskUpdate. rewrite H0,H3. simpl. trivial.
Qed.

Theorem Thread2Task_simu1_simuPred:forall (i : thInd sys)(ext : mState (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping)
  (st : AADLState sys),
getInvariant_AADL i ext st ->
forall p : ThreadPred sys i,
lpSat (Satisfy (AADLState sys) (Thread_TTS sys i)) st (P2LP i p) <->
lpSat (Satisfy (AdaState AADL2Ada) (Task_TTS AADL2Ada i))
  (mabs (AdaState AADL2Ada) (AADLState sys) AADL2Ada_mapping ext st)
  (AADLP2AdaLP i p).
Proof.
(*第七个证明目标*)
  simpl.
  intros.
  case p.
  intros.
  case thport0.
  simpl.
  intros.
  split.
  intro.
  simpl in H0.
  apply H0.
  auto.
  simpl.
  tauto.
Qed.


Theorem Thread2Task_simu1: 
  forall i, simu _ _ AADL2Ada_mapping (ThreadPred sys i) (Task_TTS AADL2Ada i) (Thread_TTS sys i) (AADLP2AdaLP i) (P2LP i).
Proof.

  intros.
  split with (getInvariant_AADL i).
  revert i.
  apply Thread2Task_simu1_InvInit.
  revert i.
  apply Thread2Task_simu1_InvDelay.
  revert i.
  apply Thread2Task_simu1_InvNext.
  revert i.
  apply Thread2Task_simu1_simuInit.
  revert i.
  apply Thread2Task_simu1_simuDelay.
  revert i.
  apply Thread2Task_simu1_simuNext.
  revert i.
  apply Thread2Task_simu1_simuPred.
Qed.
 

Record getAuxiliary_Ada: Type := mkExtState {
  eNextPeriod: thInd sys -> Time
}.

Definition AdaVars2Sys (ext: getAuxiliary_Ada) (st: AdaState AADL2Ada): AADLState sys :=
  let (tm,env,ts,tu) := st in 
  mkAADLState sys
    (fun i ip => env (inputs i ip))
    (fun i op => env (outputs i op))
    (fun i => eNextPeriod ext i)
    tm
    (fun i => env (tstates i)).

Definition getTaskUpdate2 (i: thInd sys) (ext: getAuxiliary_Ada) (env: forall v, AdaValue v) (d:Time):TaskUpdate AADL2Ada :=
  match env (tstates i) with
    Idle => 
    (mkTU AADL2Ada d
        (isUsed i)
        (fun v c => 
        match v return AdaValue v with
          inputs i1 ip => env (outputs (src sys i1 ip) (srcp sys i1 ip))
        | outputs i1 op => env (outputs i1 op)
        | tstates i1 => Dispatched
      end
    ))
  | Dispatch =>
    (mkTU AADL2Ada (eNextPeriod ext i)
      (isUsed i)
      (fun v c => 
        match v return AdaValue v with
            inputs i1 ip => env (inputs i1 ip)
          | outputs i1 op => (Computation (thread sys i1) (fun ip => env (inputs i1 ip)) op)
          | tstates i1 => Idle
        end
      ))
  end.

Record getInvariant_Ada i (ext: getAuxiliary_Ada) (st: AdaState AADL2Ada): Prop := mkTaskInv {
  Idate:forall u,taskupdate AADL2Ada st i = u -> date AADL2Ada u @<= eNextPeriod ext i;
  Iupd: getTaskUpdate2 i ext (currentEnv AADL2Ada st) (currentTime AADL2Ada st) = taskupdate AADL2Ada st i;
  Iidle: currentEnv AADL2Ada st (tstates i) = Idle -> currentTime AADL2Ada st = eNextPeriod ext i;
  Icurr: currentTime AADL2Ada st @<= eNextPeriod ext i
}.

Definition Ada2AADL_mapping: mapping (AADLState sys) (AdaState AADL2Ada) := mkMapping
  (AADLState sys)  (AdaState AADL2Ada) getAuxiliary_Ada
  (fun st: AdaState AADL2Ada => mkExtState (fun i:thInd sys => Zero))
  (fun (ext: getAuxiliary_Ada) (st: AdaState AADL2Ada) =>
        mkExtState (fun i:thInd sys => match currentEnv AADL2Ada st (tstates i) with
                          Idle => currentTime AADL2Ada st @+ (Period (thread sys i))
                        | Dispatched => eNextPeriod ext i
                        end))
  (fun (ext: getAuxiliary_Ada) (st: AdaState AADL2Ada) (d:Time) => ext) AdaVars2Sys.


Hypothesis equive : forall (st:AdaState AADL2Ada)(i:thInd sys)(env:Env AdaVars AdaValue),(taskState AADL2Ada st i = Ready -> env (tstates i)= Idle) /\ (taskState AADL2Ada st i = Running -> env (tstates i)= Dispatched).
(*Proof.
Admitted.*)

Theorem Thread2Task_simu2_InvInit:forall (i : thInd sys)(st : AdaState AADL2Ada) ,
Init (AdaState AADL2Ada) (Task_TTS AADL2Ada i) st ->
getInvariant_Ada i
  (mInit (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping st) st.
Proof.
  simpl.
  intros.
  inversion_clear H.
  elim tInitupdate0.
  simpl.
  intro.
  case x. (*分成两个目标，记为A1，A2*)
  (*A1目标*)
  simpl.
  intros.
  inversion H.
  split. (*分成四个小目标，以B进行标记*)
  (*B1目标   A1-B1*)
  intros.
  simpl in *.
  rewrite H2 in H1.
  rewrite H1.
  simpl.
  apply tle_refl.
  (*B2目标   A1-B2*)
  unfold getTaskUpdate2.
  simpl.
  rewrite H0.
  rewrite H1.
  rewrite tInitTime0.
  f_equal.
  apply env_eq.
  intro.
  case x0. (*生成三种情况，以C进行标记*)
  (*C1目标   A1-B2-C1*)
  simpl.
  intros.
  revert i1.
  rewrite <- y.
  intros.
  case (ind_eq_dec sys i i).
  trivial.
  intros.
  contradiction n.
  trivial.
  (*C2目标   A1-B2-C2*)
  intros.
  trivial.
  (*C3目标   A1-B2-C3*)
  intros.
  rewrite <- y.
  case (ind_eq_dec sys i i).
  trivial.
  intros.
  contradiction n.
  trivial.
  (*B3目标   A1-B3*)
  simpl.
  intros.
  apply tInitTime0.
  (*B4目标   A1-B4*)
  simpl.
  rewrite tInitTime0.
  apply tle_refl.
  (*A2目标*)
  simpl.
  intros.
  inversion_clear H.
  split. (*分成四个小目标，以B进行标记*)
  (*B1目标   A2-B1*)
  intros.
  simpl.
  rewrite H1 in H.
  rewrite <- H.
  simpl.
  apply tle_refl.
  (*B2目标   A2-B2*)
  unfold getTaskUpdate2.
  simpl.
  rewrite H0.
  rewrite H1.
  f_equal.
  apply env_eq.
  intro.
  case x0. (*生成三种情况，以C进行标记*)
  (*C1目标   A2-B2-C1*)
  (*intros.
  revert i1.
  rewrite <- y.
  intros.*)
  trivial.
  (*C2目标   A2-B2-C2*)
  simpl.
  intros.
  revert o.
  rewrite <- y.
  intros.
  case (ind_eq_dec sys i i).
  trivial.
  intros.
  contradiction n.
  trivial.
  (*C3目标   A2-B2-C3*)
  simpl.
  intros.
  rewrite <- y.
  case (ind_eq_dec sys i i).
  trivial.
  intros.
  contradiction n.
  trivial.
  (*B3目标   A2-B3*)
  intros.
  rewrite H0 in H.
  discriminate H.
  (*B4目标   A2-B4*)
  simpl.
  rewrite tInitTime0.
  apply tle_refl.
Qed.


Theorem Thread2Task_simu2_InvDelay:forall (i : thInd sys)(ex1 : mState (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping)
  (st1 st2 : AdaState AADL2Ada) (d : Time),
Delay (AdaState AADL2Ada) (Task_TTS AADL2Ada i) st1 d st2 ->
getInvariant_Ada i ex1 st1 ->
getInvariant_Ada i
  (mDelay (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping ex1 st1 d) st2.
Proof.
  (*第二个证明目标*)
  simpl.
  intros.
  inversion_clear H.
  inversion_clear H2.
  generalize dependent st1. intro st1. case st1. simpl. intros.
  generalize dependent st2. intro st2. case st2. simpl. intros.
  inversion_clear H0.
  simpl in Idate0,Iupd0,Iidle0,Icurr0.
  split. (*拆分为四个目标，用A进行标记*)
  (*A1目标*)
  simpl.
  intros.
  apply Idate0.
  rewrite <- H6.
  apply H0.
  (*A2目标*)
  simpl.
  rewrite H6.
  rewrite <- Iupd0.
  unfold getTaskUpdate2.
  simpl.
  rewrite (H7 (tstates i) eq_refl).
  case_eq (currentEnv0 (tstates i)). (*分为两种情况，以B进行标记*)
  (*A2-B1目标*)
  intros.
  apply False_ind.
  unfold getTaskUpdate2 in Iupd0.
  rewrite H0 in Iupd0.
  simpl in Iupd0.
  rewrite <- Iupd0 in H3.
  simpl in H3.
  generalize (tplus_le_0 _ _ H3). 
  intro.
  rewrite H2 in H1.
  apply (tlt_irrefl _ H1).
  (*A2-B2目标*)
  simpl.
  intros.
  f_equal.
  apply env_eq.
  intro.
  case x. (*分为三种情况，以C进行标记*)
  (*A2-B2-C1目标*)
  simpl.
  intros.
  rewrite (H7 (inputs i0 i1)).
  trivial.
  simpl.
  apply y.
  (*A2-B2-C2目标*)
  intros.
  apply ComputationWF.
  intros.
  rewrite (H7 (inputs i0 i1)).
  trivial.
  apply y.
  (*A2-B2-C3目标*)
  trivial.
  (*A3目标*)
  simpl.
  rewrite (H7 (tstates i) eq_refl).
  intros.
  unfold getTaskUpdate2 in Iupd0.
  rewrite H0 in Iupd0.
  rewrite <- Iupd0 in H3.
  simpl in H3.
  generalize (tplus_le_0 _ _ H3).
  intros.
  rewrite H4,H2,tplus_n_O.
  apply Iidle0.
  apply H0.
  (*A4目标*)
  simpl.
  case_eq (currentEnv0 (tstates i)). (*分为两个目标，以B进行标记*)
  (*A4-B1目标*)
  intros.
  unfold getTaskUpdate2 in Iupd0.
  rewrite H0 in Iupd0.
  simpl in Iupd0.
  rewrite <- Iupd0 in H3.
  simpl in H3.
  generalize (tplus_le_0 _ _ H3).
  intros.
  rewrite H4,H2,tplus_n_O.
  apply Icurr0.
  (*A4-B2目标*)
  intros.
  unfold getTaskUpdate2 in Iupd0.
  rewrite H0 in Iupd0.
  simpl in Iupd0.
  rewrite <- Iupd0 in H3.
  simpl in H3.
  rewrite <- H4 in H3.
  apply H3.
Qed.

Theorem Thread2Task_simu2_InvNext:forall (i : thInd sys)(ex1 : mState (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping)
  (st1 st2 : AdaState AADL2Ada),
Next (AdaState AADL2Ada) (Task_TTS AADL2Ada i) st1 st2 ->
getInvariant_Ada i ex1 st1 ->
getInvariant_Ada i
  (mNext (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping ex1 st1) st2.
Proof.
  (*第三个证明目标*)
  simpl.
  intros.
  inversion_clear H. (*分为三种情况，以A进行标记*)
  (*A1目标*)
  simpl in *.
  generalize (equive st1 i). intros.
  generalize dependent st1. intro st1. case st1. clear st1. simpl. intros.
  generalize (H currentEnv0). intros. inversion_clear H7. clear H H9.
  generalize (H8 H1). intros. clear H8.
  generalize (equive st2 i). intros.
  generalize dependent st2. intro st2. case st2. clear st2. simpl. intros.
  generalize (H7 currentEnv1). intros. inversion_clear H8. clear H7 H9.
  generalize (H10 H6). intros. clear H10.
  simpl in *.
  rewrite H2 in *|-*.
  inversion_clear H0.
  simpl in *.
  unfold getTaskUpdate2 in Iupd0.
  case_eq (currentEnv0 (tstates i)). (*分为2种情况，以B进行标记*)
  (*A1-B1目标*)
  intros.
  rewrite H in Iupd0.
  simpl in Iupd0.
  rewrite <- Iupd0 in H3.
  generalize (H3 _ eq_refl eq_refl).
  clear H3.
  simpl.
  intros.
  elim H5.
  intro.
  case x.
  unfold doComplete,doDispatch.
  simpl.
  intros.
  inversion_clear H8.
  rewrite (H3 (tstates i) eq_refl) in H9.
  discriminate H9.
  unfold doComplete,doDispatch.
  simpl.
  intros.
  inversion_clear H8.
  split. (*分为四种情况，以C进行标记*)
  (*A1-B1-C1目标*)
  simpl.
  intros.
  rewrite H.
  rewrite H10 in H8.
  rewrite <- H8.
  simpl.
  apply tle_refl.
  (*A1-B1-C2目标*)
  simpl.
  rewrite H10.
  unfold getTaskUpdate2.
  rewrite H9.
  simpl.
  rewrite H.
  f_equal.
  apply env_eq.
  intro.
  case x0.
  simpl.
  trivial.
  simpl.
  intros.
  revert o.
  rewrite <- y.
  case (ind_eq_dec sys i i).
  intros.
  trivial.
  intros.
  contradiction n.
  trivial.
  simpl.
  intros.
  rewrite y.
  case (ind_eq_dec sys t t).
  trivial.
  intros.
  contradiction n.
  trivial.
  (*A1-B1-C3目标*)
  simpl.
  intros.
  rewrite H9 in H8.
  discriminate H8.
  (*A1-B1-C4目标*)
  simpl.
  rewrite H.
  apply tle_plus_l.
  (*A1-B2目标*)
  intros.
  split. (*分为四个目标*)
  (*A1-B2-C1目标*)
  simpl.
  intros.
  rewrite H0.
  rewrite H0 in Iupd0.
  simpl in Iupd0.
  elim H5.
  intro.
  case x.
  simpl.
  intros.
  inversion_clear H9.
  rewrite H11 in H8.
  rewrite <- H8.
  simpl.
  rewrite tplus_n_O .
  apply Icurr0.
  simpl.
  intros.
  inversion_clear H9.
  simpl in H11.
  case (tle_lt_eq_dec _ _ Icurr0).
  intros.
  rewrite H4 in H8.
  intros.
  apply Idate0.
  apply H8.
  intro.
  rewrite <- Iupd0 in H9.
  generalize (H9 _ eq_refl).
  simpl.
  intros.
  rewrite H12 in t.
  apply (tlt_irrefl _ t).
  intros.
  rewrite e in *.
  rewrite <- Iupd0 in H3.
  generalize (H3 _ eq_refl eq_refl).
  simpl.
  intro.
  generalize (H9 (tstates i) eq_refl).
  intro.
  rewrite H12 in H10.
  discriminate H10.
  (*A1-B2-C2目标*)
  simpl.
  rewrite H in Iupd0.
  elim H5.
  intro.
  case x.
  simpl.
  intros.
  inversion_clear H8.
  unfold getTaskUpdate2.
  rewrite H9.
  rewrite H10.
  rewrite tplus_n_O.
  f_equal.
  apply env_eq.
  intro.
  case x0.
  simpl.
  intros.
  case (ind_eq_dec).
  trivial.
  intros.
  contradiction n.
  simpl.
  trivial.
  simpl.
  intros.
  case (ind_eq_dec sys i t).
  trivial.
  intros.
  contradiction n.
  (*A1-B2-C3目标*)
  rewrite H0 in H.
  discriminate H.
  (*A1-B2-C4目标*)
  simpl.
  rewrite H0 in H.
  discriminate H.
  simpl.
  rewrite H0.
  apply Icurr0.
  (*A2目标*)
  simpl in *.
  generalize dependent st1. intro st1. case st1. clear st1. simpl. intros.
  generalize (equive st2 i). intros.
  generalize dependent st2. intro st2. case st2. clear st2. simpl. intros.
  generalize (H currentEnv1). intros. inversion_clear H8. clear H H10.
  generalize (H9 H7). intro te. clear H9.
  simpl in *.
  rewrite H2 in *|-*.
  inversion_clear H0.
  simpl in *.
  unfold getTaskUpdate2 in Iupd0.
  case_eq (currentEnv0 (tstates i)). (*分为2种情况，以B进行标记*)
  (*A1-B1目标*)
  intros.
  rewrite H in Iupd0.
  simpl in Iupd0.
  rewrite <- Iupd0 in H4.
  rewrite <- H3 in H4.
  generalize (H4 _ eq_refl eq_refl).
  clear H4.
  simpl.
  intros.
  elim H6.
  intro.
  case x.
  unfold doComplete,doDispatch.
  simpl.
  intros.
  inversion_clear H4.
  rewrite (H0 (tstates i) eq_refl) in H8.
  discriminate H8.
  unfold doComplete,doDispatch.
  simpl.
  intros.
  inversion_clear H4.
  split. (*分为四种情况，以C进行标记*)
  (*A1-B1-C1目标*)
  simpl.
  intros.
  rewrite H.
  rewrite H9 in H4.
  rewrite <- H4.
  simpl.
  rewrite <- H3.
  apply tle_refl.
  (*A1-B1-C2目标*)
  simpl.
  rewrite H9.
  unfold getTaskUpdate2.
  rewrite H8.
  simpl.
  rewrite H.
  f_equal.
  rewrite <- H3.
  trivial.
  apply env_eq.
  intro.
  case x0.
  simpl.
  trivial.
  simpl.
  intros.
  revert o.
  rewrite <- y.
  case (ind_eq_dec sys i i).
  intros.
  trivial.
  intros.
  contradiction n.
  trivial.
  simpl.
  intros.
  rewrite y.
  case (ind_eq_dec sys t t).
  trivial.
  intros.
  contradiction n.
  trivial.
  (*A1-B1-C3目标*)
  simpl.
  intros.
  rewrite H4 in H8.
  discriminate H8.
  (*A1-B1-C4目标*)
  simpl.
  rewrite H.
  rewrite <- Iupd0.
  simpl.
  rewrite H3.
  apply tle_plus_l.
  (*A1-B2目标*)
  intros.
  split. (*分为四个目标*)
  (*A1-B2-C1目标*)
  simpl.
  intros.
  rewrite H.
  rewrite H in Iupd0.
  simpl in Iupd0.
  elim H6.
  intro.
  case x.
  simpl.
  intros.
  inversion_clear H8.
  rewrite H10 in H0.
  rewrite <- H0.
  simpl.
  rewrite tplus_n_O .
  rewrite H3.
  rewrite <- Iupd0.
  simpl.
  apply tle_refl.
  simpl.
  intros.
  inversion_clear H8.
  case (tle_lt_eq_dec _ _ Icurr0).
  intros.
  rewrite H5 in H0.
  intros.
  apply Idate0.
  apply H0.
  intro.
  rewrite <- Iupd0 in H8.
  generalize (H8 _ eq_refl).
  simpl.
  intros.
  rewrite <- Iupd0 in t.
  simpl in t.
  apply (tlt_irrefl _ t).
  intros.
  rewrite e in *.
  rewrite <- Iupd0 in H4.
  rewrite H3 in H4.
  generalize (H4 _ eq_refl eq_refl).
  simpl.
  intro.
  generalize (H8 (tstates i) eq_refl).
  intro.
  rewrite H11 in H9.
  discriminate H9.
  (*A1-B2-C2目标*)
  simpl.
  rewrite H in Iupd0.
  elim H6.
  intro.
  case x.
  simpl.
  intros.
  inversion_clear H0.
  unfold getTaskUpdate2.
  rewrite H8.
  rewrite H9.
  rewrite tplus_n_O.
  f_equal.
  apply env_eq.
  intro.
  case x0.
  simpl.
  intros.
  case (ind_eq_dec).
  trivial.
  intros.
  contradiction n.
  simpl.
  trivial.
  simpl.
  intros.
  case (ind_eq_dec sys i t).
  trivial.
  intros.
  contradiction n.
  (*A1-B2-C3目标*)
  unfold doComplete.
  simpl.
  intros.
  inversion_clear H0.
  rewrite H8 in te.
  discriminate te.
  simpl.
  intros.
  rewrite H.
  rewrite H in Iupd0.
  rewrite <- Iupd0 in H3.
  simpl in H3.
  trivial.
  simpl.
  rewrite H.
  rewrite H in Iupd0.
  rewrite <- Iupd0 in H3.
  simpl in H3.
  rewrite H3.
  apply tle_refl.

  generalize (equive st1 i). intros.
  generalize dependent st1. intro st1. case st1. clear st1. simpl. intros.
  generalize (H currentEnv0). intros. inversion_clear H8. clear H H9.
  generalize (H10 H1). intros. clear H10.
  generalize (equive st2 i). intros.
  generalize dependent st2. intro st2. case st2. clear st2. simpl. intros.
  generalize (H8 currentEnv1). intros. inversion_clear H9. clear H8 H10.
  generalize (H11 H6). intros. clear H11.
  simpl in *. clear H1 H6.
  inversion_clear H0.
  simpl in *.
  split.
  simpl. rewrite H. intros. rewrite H5 in H0. 
  unfold getTaskUpdate2 in Iupd0. rewrite H in Iupd0.
  rewrite <- Iupd0 in H0. rewrite <- H0. simpl. apply tle_refl.
  intros. unfold getTaskUpdate2 in Iupd0. rewrite H in Iupd0.
  rewrite <- Iupd0 in H1. rewrite <- H1. simpl. trivial.
  unfold getTaskUpdate2. simpl. rewrite H8.
  simpl. rewrite H5. 
  unfold getTaskUpdate2 in Iupd0. rewrite H in Iupd0.
  rewrite <- Iupd0. rewrite H.
  f_equal. apply env_eq.
  intro. case x.
  simpl. intros. revert i1. rewrite <- y. intros. rewrite (H4 (inputs i i1)). trivial. simpl. trivial.
  simpl. intros. apply ComputationWF. rewrite <- y. intros. rewrite (H4 (inputs i i1)). trivial. simpl. trivial.
  simpl. trivial.
  intros. unfold getTaskUpdate2 in Iupd0. rewrite H in Iupd0. rewrite <- Iupd0 in H0. rewrite <- H0. simpl. trivial.
  simpl. intros. rewrite H0 in H8. discriminate H8.
  simpl. rewrite H. rewrite H3. trivial.
Qed.

Theorem Thread2Task_simu2_simuInit:forall (i : thInd sys)(st : AdaState AADL2Ada),
Init (AdaState AADL2Ada) (Task_TTS AADL2Ada i) st ->
Init (AADLState sys) (Thread_TTS sys i)
  (mabs (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping
     (mInit (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping st) st).
Proof.
  (*第四个证明目标*)
  simpl.
  intros.
  inversion_clear H.
  inversion_clear tInitupdate0.
  inversion_clear H.
  generalize dependent st. intro st. case st. clear st. simpl. intros.
  intros.
  split.
  simpl.
  trivial.
  simpl.
  trivial.
  simpl.
  apply (tInitenv0 (tstates i) eq_refl).
Qed.


Theorem Thread2Task_simu2_simuNext:forall (i : thInd sys)(ex1 : mState (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping)
  (st1 st2 : AdaState AADL2Ada),
Next (AdaState AADL2Ada) (Task_TTS AADL2Ada i) st1 st2 ->
getInvariant_Ada i ex1 st1 ->
Next (AADLState sys) (Thread_TTS sys i)
  (mabs (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping ex1 st1)
  (mabs (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping
     (mNext (AADLState sys) (AdaState AADL2Ada) Ada2AADL_mapping ex1 st1) st2).
Proof.
  (*第六个证明目标*)
  simpl.
  intros.
  inversion_clear H. (*目标一分为三*)

  (*当前证明taskDispatched*)
  generalize (equive st1 i). intros.
  generalize dependent st1. intro st1. case st1.  simpl. intros.
  generalize (H currentEnv0). intros. inversion_clear H7. clear H H9.
  generalize (equive st2 i). intros.
  generalize dependent st2. intro st2. case st2.  simpl. intros.
  generalize (H currentEnv1). intros. inversion_clear H7. clear H9 H.
  generalize (H8 H1). intros. generalize (H10 H6). intros. clear H8 H10.
  simpl in *.
  rewrite H2 in *|-*.
  inversion_clear H0.
  simpl in *. 
  unfold getTaskUpdate2 in Iupd0.
  rewrite H in Iupd0.
  rewrite <- Iupd0 in H3.
  generalize (H3 _ eq_refl eq_refl).
  simpl. 
  intros.
  apply thDispatch.
  simpl.
  trivial.
  simpl.
  trivial.
  simpl. intros. rewrite (H0 (inputs i ip)). trivial. simpl. trivial.
  simpl. intros. rewrite (H0 (outputs i op)). trivial. simpl. trivial.
  simpl. rewrite H. f_equal. apply Iidle0. trivial.
  simpl. trivial.

  (*当前证明taskComplete*)
  generalize (equive st1 i). intros.
  generalize dependent st1. intro st1. case st1.  simpl. intros.
  generalize (H currentEnv0). intros. inversion_clear H8. clear H9 H.
  generalize (equive st2 i). intros.
  generalize dependent st2. intro st2. case st2.  simpl. intros.
  generalize (H currentEnv1). intros. inversion_clear H8. clear H11 H.
  generalize (H10 H1). intros. generalize (H9 H7). intros. clear H9 H10.
  simpl in *.
  inversion_clear H0.
  simpl in *. 
  unfold getTaskUpdate2 in Iupd0.
  rewrite H in Iupd0.
  rewrite <- Iupd0 in H4.
  rewrite <- Iupd0 in H2.
  simpl in H2.
  rewrite <- H2 in H4.
  rewrite <- H3 in H4.
  generalize (H4 _ eq_refl eq_refl).
  simpl. 
  intros.
  apply thComplete.
  simpl.
  trivial.
  simpl.
  trivial.
  simpl.
  trivial.
  simpl.
  trivial.
  simpl.
  intros.
  apply (H0 (inputs i ip)).
  simpl.
  trivial.
  simpl.
  intros.
  generalize (H0 (outputs i op)).
  simpl.
  intros.
  apply H9.
  trivial.
  simpl.
  rewrite H.
  trivial.

  (*证明taskcompute*)
  generalize (equive st1 i). intros.
  generalize dependent st1. intro st1. case st1.  simpl. intros.
  generalize (H currentEnv0). intros. inversion_clear H8. clear H9 H.
  generalize (equive st2 i). intros.
  generalize dependent st2. intro st2. case st2.  simpl. intros.
  generalize (H currentEnv1). intros. inversion_clear H8. clear H9 H.
  generalize (H10 H1). intros. generalize (H11 H6). intros. clear H10 H11.
  simpl in *.
  inversion_clear H0.
  simpl in *.
  unfold getTaskUpdate2 in Iupd0.
  rewrite H in Iupd0.
  apply thCompute.
  simpl.
  trivial.
  simpl.
  rewrite <- Iupd0 in H2.
  simpl in H2.
  trivial.
  simpl.
  trivial.
  simpl.
  trivial.
  simpl.
  intros.
  apply (H4 (inputs i ip)).
  simpl.
  trivial.
  simpl.
  intros.
  apply (H4 (outputs i op)).
  simpl.
  trivial.
  simpl.
  rewrite H.
  trivial.
Qed.



End AADL2Ada.